es{-}in{-}port(${\it es}$;$l$;${\it tg}$)($e$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$if es{-}kind(${\it es}$; $e$) = rcv($l$,${\it tg}$) then inl es{-}val(${\it es}$; $e$)  else inr $\cdot$  fi